(defconst guru-font-lock-keywords
  '(("%-\\(.\\|[\r\n]\\)*?-%" ;; multi-line comment
     . font-lock-comment-face)
    ("%.*" ;; single-line comment
     . font-lock-comment-face)
    ("\\(Define\\|Inductive\\)[\t ]*\\(spec\\)?[\t ]*\\([A-Za-z0-9_]*\\)[\n\t ]*\\(:.*\\)" ;;?:=.*"
     3 font-lock-function-name-face)
    ("fun[\t ]*\\([A-Za-z0-9_]*\\)"
     1 font-lock-function-name-face)
;;    (("[\t ]*(\\(.*\\):\\(.*\\)[\t ]*)"
;;      (1 'font-lock-variable-face)
;;      (2 'font-lock-type-face)))
    ;;("\(abbrev|let\)[\t ]*(\.*\)[\t ]=)"
     ;; 2 font-lock-variable-face)
  ))

(defconst guru-font-lock-defaults
  '(guru-font-lock-keywords t))

(define-derived-mode guru-mode fundamental-mode "Guru"
  "Major more for editing guru files."

  (setq comment-start "%")
  (setq comment-start-skip "%+ *")

  (make-local-variable 'font-lock-defaults)
  (setq font-lock-defaults guru-font-lock-defaults))

(add-to-list 'auto-mode-alist '(".g\\'" . guru-mode))

(provide 'guru-mode)

;;   '("**" "*" "do" "fun" "cast"
;;     "terminates" "(" "abort"
;;     "let" "abbrev" "eabbrev" "match"
;;     "Fun" "type" "<" "@<" "@"
;;     "@" "foralli" "[" "case"
;;     "terminates-case" "!" "existsi"
;;     "andi" "existse_term" "existse" "truei"
;;     "diseqi" "True" "False" "voidi" "void"
;;     "join" "evalto" "eval" "hypjoin" "refl"
;;     "symm" "transs" "trans" "cong" "ncong"
;;     "inj" "clash" "aclash" "cinv" "subst"
;;     "show" "contra" "induction" "Forall"
;;     "Exists" "{" "cutoff" "cind" "impossible"
;;     "size" "0x" "\'" "\"" ")" "]" ">"
;;     "." "=" "|")
;;   '(("%-.*-%" 1 'font-lock-comment-start
;;     ("=" . 'font-lock-operator)
;;     (";" . 'font-lock-builtin))
;;   '("\\.g$")
;;   (list (lambda () (setq comment-start "%")))
;;   "A mode for Guru files"
;; )

